↳ Prolog
↳ PrologToPiTRSProof
goal_in(X) → U6(X, s2t_in(X, T))
s2t_in(0, nil) → s2t_out(0, nil)
s2t_in(s(X), node(nil, Y, nil)) → s2t_out(s(X), node(nil, Y, nil))
s2t_in(s(X), node(T, Y, nil)) → U5(X, T, Y, s2t_in(X, T))
s2t_in(s(X), node(nil, Y, T)) → U4(X, Y, T, s2t_in(X, T))
s2t_in(s(X), node(T, Y, T)) → U3(X, T, Y, s2t_in(X, T))
U3(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, T))
U4(X, Y, T, s2t_out(X, T)) → s2t_out(s(X), node(nil, Y, T))
U5(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, nil))
U6(X, s2t_out(X, T)) → U7(X, tree_in(T))
tree_in(node(L, X, R)) → U1(L, X, R, tree_in(L))
tree_in(nil) → tree_out(nil)
U1(L, X, R, tree_out(L)) → U2(L, X, R, tree_in(R))
U2(L, X, R, tree_out(R)) → tree_out(node(L, X, R))
U7(X, tree_out(T)) → goal_out(X)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
goal_in(X) → U6(X, s2t_in(X, T))
s2t_in(0, nil) → s2t_out(0, nil)
s2t_in(s(X), node(nil, Y, nil)) → s2t_out(s(X), node(nil, Y, nil))
s2t_in(s(X), node(T, Y, nil)) → U5(X, T, Y, s2t_in(X, T))
s2t_in(s(X), node(nil, Y, T)) → U4(X, Y, T, s2t_in(X, T))
s2t_in(s(X), node(T, Y, T)) → U3(X, T, Y, s2t_in(X, T))
U3(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, T))
U4(X, Y, T, s2t_out(X, T)) → s2t_out(s(X), node(nil, Y, T))
U5(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, nil))
U6(X, s2t_out(X, T)) → U7(X, tree_in(T))
tree_in(node(L, X, R)) → U1(L, X, R, tree_in(L))
tree_in(nil) → tree_out(nil)
U1(L, X, R, tree_out(L)) → U2(L, X, R, tree_in(R))
U2(L, X, R, tree_out(R)) → tree_out(node(L, X, R))
U7(X, tree_out(T)) → goal_out(X)
GOAL_IN(X) → U61(X, s2t_in(X, T))
GOAL_IN(X) → S2T_IN(X, T)
S2T_IN(s(X), node(T, Y, nil)) → U51(X, T, Y, s2t_in(X, T))
S2T_IN(s(X), node(T, Y, nil)) → S2T_IN(X, T)
S2T_IN(s(X), node(nil, Y, T)) → U41(X, Y, T, s2t_in(X, T))
S2T_IN(s(X), node(nil, Y, T)) → S2T_IN(X, T)
S2T_IN(s(X), node(T, Y, T)) → U31(X, T, Y, s2t_in(X, T))
S2T_IN(s(X), node(T, Y, T)) → S2T_IN(X, T)
U61(X, s2t_out(X, T)) → U71(X, tree_in(T))
U61(X, s2t_out(X, T)) → TREE_IN(T)
TREE_IN(node(L, X, R)) → U11(L, X, R, tree_in(L))
TREE_IN(node(L, X, R)) → TREE_IN(L)
U11(L, X, R, tree_out(L)) → U21(L, X, R, tree_in(R))
U11(L, X, R, tree_out(L)) → TREE_IN(R)
goal_in(X) → U6(X, s2t_in(X, T))
s2t_in(0, nil) → s2t_out(0, nil)
s2t_in(s(X), node(nil, Y, nil)) → s2t_out(s(X), node(nil, Y, nil))
s2t_in(s(X), node(T, Y, nil)) → U5(X, T, Y, s2t_in(X, T))
s2t_in(s(X), node(nil, Y, T)) → U4(X, Y, T, s2t_in(X, T))
s2t_in(s(X), node(T, Y, T)) → U3(X, T, Y, s2t_in(X, T))
U3(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, T))
U4(X, Y, T, s2t_out(X, T)) → s2t_out(s(X), node(nil, Y, T))
U5(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, nil))
U6(X, s2t_out(X, T)) → U7(X, tree_in(T))
tree_in(node(L, X, R)) → U1(L, X, R, tree_in(L))
tree_in(nil) → tree_out(nil)
U1(L, X, R, tree_out(L)) → U2(L, X, R, tree_in(R))
U2(L, X, R, tree_out(R)) → tree_out(node(L, X, R))
U7(X, tree_out(T)) → goal_out(X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
GOAL_IN(X) → U61(X, s2t_in(X, T))
GOAL_IN(X) → S2T_IN(X, T)
S2T_IN(s(X), node(T, Y, nil)) → U51(X, T, Y, s2t_in(X, T))
S2T_IN(s(X), node(T, Y, nil)) → S2T_IN(X, T)
S2T_IN(s(X), node(nil, Y, T)) → U41(X, Y, T, s2t_in(X, T))
S2T_IN(s(X), node(nil, Y, T)) → S2T_IN(X, T)
S2T_IN(s(X), node(T, Y, T)) → U31(X, T, Y, s2t_in(X, T))
S2T_IN(s(X), node(T, Y, T)) → S2T_IN(X, T)
U61(X, s2t_out(X, T)) → U71(X, tree_in(T))
U61(X, s2t_out(X, T)) → TREE_IN(T)
TREE_IN(node(L, X, R)) → U11(L, X, R, tree_in(L))
TREE_IN(node(L, X, R)) → TREE_IN(L)
U11(L, X, R, tree_out(L)) → U21(L, X, R, tree_in(R))
U11(L, X, R, tree_out(L)) → TREE_IN(R)
goal_in(X) → U6(X, s2t_in(X, T))
s2t_in(0, nil) → s2t_out(0, nil)
s2t_in(s(X), node(nil, Y, nil)) → s2t_out(s(X), node(nil, Y, nil))
s2t_in(s(X), node(T, Y, nil)) → U5(X, T, Y, s2t_in(X, T))
s2t_in(s(X), node(nil, Y, T)) → U4(X, Y, T, s2t_in(X, T))
s2t_in(s(X), node(T, Y, T)) → U3(X, T, Y, s2t_in(X, T))
U3(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, T))
U4(X, Y, T, s2t_out(X, T)) → s2t_out(s(X), node(nil, Y, T))
U5(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, nil))
U6(X, s2t_out(X, T)) → U7(X, tree_in(T))
tree_in(node(L, X, R)) → U1(L, X, R, tree_in(L))
tree_in(nil) → tree_out(nil)
U1(L, X, R, tree_out(L)) → U2(L, X, R, tree_in(R))
U2(L, X, R, tree_out(R)) → tree_out(node(L, X, R))
U7(X, tree_out(T)) → goal_out(X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
TREE_IN(node(L, X, R)) → U11(L, X, R, tree_in(L))
U11(L, X, R, tree_out(L)) → TREE_IN(R)
TREE_IN(node(L, X, R)) → TREE_IN(L)
goal_in(X) → U6(X, s2t_in(X, T))
s2t_in(0, nil) → s2t_out(0, nil)
s2t_in(s(X), node(nil, Y, nil)) → s2t_out(s(X), node(nil, Y, nil))
s2t_in(s(X), node(T, Y, nil)) → U5(X, T, Y, s2t_in(X, T))
s2t_in(s(X), node(nil, Y, T)) → U4(X, Y, T, s2t_in(X, T))
s2t_in(s(X), node(T, Y, T)) → U3(X, T, Y, s2t_in(X, T))
U3(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, T))
U4(X, Y, T, s2t_out(X, T)) → s2t_out(s(X), node(nil, Y, T))
U5(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, nil))
U6(X, s2t_out(X, T)) → U7(X, tree_in(T))
tree_in(node(L, X, R)) → U1(L, X, R, tree_in(L))
tree_in(nil) → tree_out(nil)
U1(L, X, R, tree_out(L)) → U2(L, X, R, tree_in(R))
U2(L, X, R, tree_out(R)) → tree_out(node(L, X, R))
U7(X, tree_out(T)) → goal_out(X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
TREE_IN(node(L, X, R)) → U11(L, X, R, tree_in(L))
U11(L, X, R, tree_out(L)) → TREE_IN(R)
TREE_IN(node(L, X, R)) → TREE_IN(L)
tree_in(node(L, X, R)) → U1(L, X, R, tree_in(L))
tree_in(nil) → tree_out(nil)
U1(L, X, R, tree_out(L)) → U2(L, X, R, tree_in(R))
U2(L, X, R, tree_out(R)) → tree_out(node(L, X, R))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
U11(R, tree_out) → TREE_IN(R)
TREE_IN(node(L, R)) → TREE_IN(L)
TREE_IN(node(L, R)) → U11(R, tree_in(L))
tree_in(node(L, R)) → U1(R, tree_in(L))
tree_in(nil) → tree_out
U1(R, tree_out) → U2(tree_in(R))
U2(tree_out) → tree_out
tree_in(x0)
U1(x0, x1)
U2(x0)
From the DPs we obtained the following set of size-change graphs:
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
S2T_IN(s(X), node(T, Y, T)) → S2T_IN(X, T)
S2T_IN(s(X), node(T, Y, nil)) → S2T_IN(X, T)
S2T_IN(s(X), node(nil, Y, T)) → S2T_IN(X, T)
goal_in(X) → U6(X, s2t_in(X, T))
s2t_in(0, nil) → s2t_out(0, nil)
s2t_in(s(X), node(nil, Y, nil)) → s2t_out(s(X), node(nil, Y, nil))
s2t_in(s(X), node(T, Y, nil)) → U5(X, T, Y, s2t_in(X, T))
s2t_in(s(X), node(nil, Y, T)) → U4(X, Y, T, s2t_in(X, T))
s2t_in(s(X), node(T, Y, T)) → U3(X, T, Y, s2t_in(X, T))
U3(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, T))
U4(X, Y, T, s2t_out(X, T)) → s2t_out(s(X), node(nil, Y, T))
U5(X, T, Y, s2t_out(X, T)) → s2t_out(s(X), node(T, Y, nil))
U6(X, s2t_out(X, T)) → U7(X, tree_in(T))
tree_in(node(L, X, R)) → U1(L, X, R, tree_in(L))
tree_in(nil) → tree_out(nil)
U1(L, X, R, tree_out(L)) → U2(L, X, R, tree_in(R))
U2(L, X, R, tree_out(R)) → tree_out(node(L, X, R))
U7(X, tree_out(T)) → goal_out(X)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
S2T_IN(s(X), node(T, Y, T)) → S2T_IN(X, T)
S2T_IN(s(X), node(T, Y, nil)) → S2T_IN(X, T)
S2T_IN(s(X), node(nil, Y, T)) → S2T_IN(X, T)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
S2T_IN(s(X)) → S2T_IN(X)
From the DPs we obtained the following set of size-change graphs: